(set-logic QF_BV)
(declare-fun x0 () (_ BitVec 16))
(declare-fun x1 () (_ BitVec 1))
(declare-fun x2 () (_ BitVec 1))
(declare-fun x3 () (_ BitVec 1))
(declare-fun x4 () Bool)
(declare-fun x5 () (_ BitVec 16))
(declare-fun x6 () (_ BitVec 3))
(declare-fun x7 () (_ BitVec 16))
(declare-fun x8 () (_ BitVec 16))
(declare-fun x9 () (_ BitVec 1))
(declare-fun x10 () (_ BitVec 1))
(declare-fun x11 () (_ BitVec 16))

(assert (= x6 (_ bv6 3)))
(assert (= x1 x2))
(assert (= x9 (ite (or (= x1 (_ bv1 1)) (= x10 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
(assert (= x3 x9))
(assert (= (_ bv0 16) (ite (= x10 (_ bv1 1)) (_ bv0 16) x0)))
(assert (= x5 (_ bv611 16)))
(assert (= x7 (_ bv705 16)))
(assert (= x8 (ite x4 x5 x7)))
(assert (= x11 x8))
(assert (= (_ bv0 16) (ite (= x3 (_ bv1 1)) (_ bv0 16) x11)))

(check-sat)

(exit)
